Search for: All records

Abstract This paper presents StarV, a new tool for verifying deep neural networks (DNNs) and learning-enabled Cyber-Physical Systems (Le-CPS) using the well-known star reachability. Distinguished from existing star-based verification tools such as NNV and NNENUM and others, StarV not only offers qualitative verification techniques using Star and ImageStar reachability analysis but is also the first tool to propose using ProbStar reachability for quantitative verification of DNNs with piecewise linear activation functions and Le-CPS. Notably, it introduces a novel ProbStar Temporal Logic formalism and associated algorithms, enabling the quantitative verification of DNNs and Le-CPS’s temporal behaviors. Additionally, StarV presents a novel SparseImageStar set representation and associated reachability algorithm that allows users to verify deep convolutional neural networks and semantic segmentation networks with more memory efficiency. StarV is evaluated in comparison with state-of-the-art in many challenging benchmarks. The experiments show that StarV outperforms existing tools in many aspects, such as timing performance, scalability, and memory consumption. 

Abstract For patients who have difficulty in mechanical cleaning of dental appliances, a denture cleaner that can remove biofilm with dense extracellular polymeric substances is needed. The purpose of this study is to evaluate the efficacy of diatom complex with active micro-locomotion for removing biofilms from 3D printed dentures. The diatom complex, which is made by doping MnO₂nanosheets on diatom biosilica, is mixed with H₂O₂to generate fine air bubbles continuously. Denture base resin specimens were 3D printed in a roof shape, andPseudomonas aeruginosa(10⁷ CFU/mL) was cultured on those for biofilm formation. Cleaning solutions of phosphate-buffered saline (negative control, NC), 3% H₂O₂with peracetic acid (positive control, PC), denture cleanser tablet (DCT), 3% H₂O₂with 2 mg/mL diatom complex M (Melosira, DM), 3% H₂O₂with 2 mg/mL diatom complex A (Aulacoseira, DA), and DCT with 2 mg/mL DM were prepared and applied. To assess the efficacy of biofilm removal quantitatively, absorbance after cleaning was measured. To evaluate the stability of long-term use, surface roughness, ΔE, surface micro-hardness, and flexural strength of the 3D printed dentures were measured before and after cleaning. Cytotoxicity was evaluated using Cell Counting Kit-8. All statistical analyses were conducted using SPSS for Windows with one-way ANOVA, followed by Scheffe’s test as a post hoc (p < 0.05). The group treated with 3% H₂O₂with DA demonstrated the lowest absorbance value, followed by the groups treated with 3% H₂O₂with DM, PC, DCT, DCT + DM, and finally NC. As a result of Scheffe’s test to evaluate the significance of difference between the mean values of each group, statistically significant differences were shown in all groups based on the NC group. The DA and DM groups showed the largest mean difference though there was no significant difference between the two groups. Regarding the evaluation of physical and mechanical properties of the denture base resin, no statistically significant differences were observed before and after cleaning. In the cytotoxicity test, the relative cell count was over 70%, reflecting an absence of cytotoxicity. The diatom complex utilizing active micro-locomotion has effective biofilm removal ability and has a minimal effect in physical and mechanical properties of the substrate with no cytotoxicity. 

This paper extends the star set reachability approach to verify the robustness of feed-forward neural networks (FNNs) with sigmoidal activation functions such as Sigmoid and TanH. The main drawbacks of the star set approach in Sigmoid/TanH FNN verification are scalability, feasibility, and optimality issues in some cases due to the linear programming solver usage. We overcome this challenge by proposing a relaxed star (RStar) with symbolic intervals, which allows the usage of the back-substitution technique in DeepPoly to find bounds when overapproximating activation functions while maintaining the valuable features of a star set. RStar can overapproximate a sigmoidal activation function using four linear constraints (RStar4) or two linear constraints (RStar2), or only the output bounds (RStar0). We implement our RStar reachability algorithms in NNV and compare them to DeepPoly via robustness verification of image classification DNNs benchmarks. The experimental results show that the original star approach (i.e., no relaxation) is the least conservative of all methods yet the slowest. RStar4 is computationally much faster than the original star method and is the second least conservative approach. It certifies up to 40% more images against adversarial attacks than DeepPoly and on average 51 times faster than the star set. Last but not least, RStar0 is the most conservative method, which could only verify two cases for the CIFAR10 small Sigmoid network,δ= 0.014. However, it is the fastest method that can verify neural networks up to 3528 times faster than the star set and up to 46 times faster than DeepPoly in our evaluation. 

Deep Neural Networks (DNNs) have become a popular instrument for solving various real-world problems. DNNs’ sophisticated structure allows them to learn complex representations and features. For this reason, Binary Neural Networks (BNNs) are widely used on edge devices, such as microcomputers. However, architecture specifics and floating-point number usage result in an increased computational operations complexity. Like other DNNs, BNNs are vulnerable to adversarial attacks; even a small perturbation to the input set may lead to an errant output. Unfortunately, only a few approaches have been proposed for verifying BNNs.This paper proposes an approach to verify BNNs on continuous input space using star reachability analysis. Our approach can compute both exact and overapproximate reachable sets of BNNs with Sign activation functions and use them for verification. The proposed approach is also efficient in constructing a complete set of counterexamples in case a network is unsafe. We implemented our approach in NNV, a neural network verification tool for DNNs and learning-enabled Cyber-Physical Systems. The experimental results show that our star-based approach is less conservative, more efficient, and scalable than the recent SMT-based method implemented in Marabou. We also provide a comparison with a quantization-based tool EEVBNN.